module counter_props (
    input wire clk,
    input wire rst_n,
    input wire en,
    input wire [3:0] cnt,
    input wire ovf
);
    //初始强制复位
    initial assume(!rst_n);
    // ==============================================
    // 断言1: 复位生效后计数器必须归零且无溢出
    // 原始SVA: !rst_n |=> (cnt == 0 && !ovf)
    // ==============================================
    always @(posedge clk) begin
        if (!rst_n) begin
            assert (cnt == 4'b0 && ovf == 1'b0);
        end
    end
    // ==============================================
    // 断言2: 使能有效时计数器必须自动递增
    // 原始SVA: en && (cnt < 4'hf) |=> cnt == past_cnt + 1
    // ==============================================
    always @(posedge clk) begin
        if (rst_n && $past(rst_n)  && $past(en) && ($past(cnt) < 4'hf) ) begin
            // 检查下一个周期的值
            assert (cnt == ($past(cnt) + 1));
        end
        // 错误状态保持一个周期
    end
    // ==============================================
    // 断言3: 计数器满后必须归零并置位溢出
    // 原始SVA: en && (past_cnt == 4'hf) |=> (cnt == 0 && ovf)
    // ==============================================
    always @(posedge clk) begin
        if ($past(rst_n)&& rst_n && $past(en)&& en && ($past(cnt) == 4'hf)) begin
            assert (cnt == 4'b0 && ovf == 1'b1);
        end
    end
    // ==============================================
    // 覆盖率收集（保持原功能）
    // ==============================================
    generate
        for (genvar i = 0; i < 16; i++) begin : gen_covers
            always @(posedge clk) begin
                cover (cnt == i);
            end
        end
    endgenerate
//    always @(posedge clk) begin
//        cover (cnt == 16);
//    end
endmodule